T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
((es-initially(es; loc(e); x) = es-when(es; x; e)  T))  (x changed before e) 

latex

Definitions	if b then t else f fi , tt, b, T, es-dtype(es; i; x; T), P  Q, True, A c B, es-le(es; e; e'), x:A. B(x), P  Q, P  Q, prop{i:l}, t  T, P  Q, P  Q, EqDecider(T), x:A. B(x), guard(T), sq_type(T), SqStable(P)
Lemmas	es-first-init, sq stable subtype rel, Id sq, decidable assert, es-isconst wf, sq stable from decidable, es-when-first-discrete, true wf, squash wf, es-le-loc, es-locl wf, es-init-le, es-init wf, assert wf, iff wf, bool wf, event system wf, Id wf, es-dtype wf, es-E wf, es-when wf, es-vartype wf, es-loc wf, es-initially wf, not wf, has-changed